(declare-fun _substvar_540_ () Bool)
(declare-fun _substvar_646_ () Bool)
(declare-fun _substvar_649_ () Bool)
(declare-fun _substvar_651_ () Bool)
(declare-fun _substvar_652_ () Bool)
(declare-fun _substvar_757_ () Bool)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const i1 Int)
(declare-const i3 Int)
(declare-const i6 Int)
(declare-const i7 Int)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const i9 Int)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const i10 Int)
(push)
(assert (or v1 (and (= 493 (+ i7 5 96)) (>= i7 i6) v2 (<= i6 890) (> i1 i3 i7 i3 86) (>= 493 (- i7 i1 26)) v4 _substvar_652_) v10))
(assert _substvar_649_)
(assert (or v11 v5 (= true v10 (> 5 i3) true (distinct i6 33) true true v12 v9)))
(assert (or v5 v13 (=> (> 33 26 i1 559 (+ (div (- (+ i7 5 96) i1 26) 5) i1 i9 559)) false)))
(assert (or (= 493 (+ i7 5 96)) (and _substvar_757_ v2 (=> v0 v6) _substvar_646_ _substvar_651_ v4 _substvar_540_)))
(check-sat)
